\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$, $B$:Type, ${\it Ia}_{1}$, ${\it Ia}_{2}$:AbsInterface($A$), ${\it Ib}_{1}$, ${\it Ib}_{2}$:AbsInterface($B$),\+
\\[0ex]$g_{1}$:(E(${\it Ib}_{1}$)$\rightarrow$E(${\it Ia}_{1}$)), $g_{2}$:(E(${\it Ib}_{2}$)$\rightarrow$E(${\it Ia}_{2}$)). [\{${\it Ib}_{1}$\}? $g_{1}$ : $g_{2}$] $\in$ \{$e$:E$\mid$ \{[${\it Ib}_{1}$?${\it Ib}_{2}$]\}($e$)\} $\rightarrow$E
\-
\end{tabbing}